T:Type. 
subtype_rel(T; )
 (x:T, L:(T List). sorted(cons(x; L))  (sorted(L)  l_all(L; T; z.(x  z)))) 

latex

Definitions	x:A. B(x), P  Q, P  Q, sorted(L), P  Q, A  B, ||as||, Y, P  Q, t  T, prop{i:l}, subtype(S; T), A, False, x. t(x), int_seg(i; j), lelt(i; j; k), x(s)
Lemmas	int seg wf, length wf1, le wf, select wf, l all wf2, l member wf